Nat kind
型レベル自然数を表す型が持つ
kind
Data.Nat
での定義
code:hs
data Nat = Z | S Nat deriving (Eq, Typeable, Data)
ペアノの公理
をそのまま型レベルに定義していることがわかる
例
code:hs
{-# LANGUAGE DataKinds
#-}
type N0 = 'Z
type N1 = 'S 'Z
type N2 = 'S ('S 'Z)
type N3 = 'S ('S ('S 'Z))
...
GHC.Types
の定義は特に面白みはない
ref
GHC.TypeLits
はこれをexportしてる
Data.Type.Nat
はなに？
https://hackage.haskell.org/package/fin-0.2/docs/Data-Type-Nat.html
Data.Nat
https://hackage.haskell.org/package/fin-0.2/docs/Data-Nat.html
関連
Data.Type.Bool
https://qiita.com/aiya000/items/6e6946b2604fcaf621bb#datatypebool-
Data.Type.Equality
https://qiita.com/aiya000/items/6e6946b2604fcaf621bb#datatypeequality-
#??
なんでGHC.TypesとData.Natの両方で定義されている？
なんで定義の仕方が異なる？
https://zenn.dev/mod_poppo/books/haskell-type-level-programming/viewer/ghc-typenats